Issue3810c.agda:34,13-18
Global confluence check failed: f (Box A) (g (Box A)) can be
rewritten to either b or f (Box A) (box a).
Possible fix: add a rewrite rule with left-hand side
f (Box A) (g (Box A)) to resolve the ambiguity.
when checking confluence of the rewrite rule rewf₂ with rewg
Issue3810c.agda:40,9-13
a != b of type A
when checking that the expression refl has type a ≡ b
